"""
Reduce lambda calculus expressions.

Variable names mean things:
node: any result of parser.parse()
body: a list of nodes, usually the body of a function
params: a string of characters; the parameters of a function
func: a list [params, body]
name: a character
"""
from string import ascii_letters as CHARS

from utils import *

def getNewName(name, forbidden):
    """
    Return value for name not in forbidden. This could be name if name is not in
    forbidden.
    """
    if name not in forbidden:
        return name

    new = name
    while True:
        new = CHARS[(CHARS.index(new) + 1) % len(CHARS)]
        if new not in forbidden:
            return new
        if new == name:
            raise ValueError, 'no new name possible'

##def getNames(node, inFuncs):
##    """
##    Return a set of names contained in node.
##    
##    If inFuncs, includes those in function bodies and parameters.
##
##    >>> getNames(['a'], False)
##    set(['a'])
##    >>> getNames([['/abc', ['/x', 'xbd']]], False)
##    set([])
##    >>> list(sorted(getNames([['/abc', ['/x', 'xbd']]], True)))
##    ['a', 'b', 'c', 'd', 'x']
##    """
##    if isName(node):
##        return set(node)
##    elif isFunc(node):
##        if not inFuncs:
##            return ''
##
##        params, body = splitFunc(node)
##        return set(params) | getNames(body, inFuncs)
##
##    return reduce(
##            set.union,
##            (getNames(innerNode, inFuncs) for innerNode in node),
##            set()
##            )

##def reduceFunc(func, args):
##    params, body = splitFunc(func)
##
##    argNames = getNames(args, True)
##    print argNames
##    nameToNew = getNameToNew(body, argNames)
##    print nameToNew
##
##    newBody = substitute(body, nameToNew)
##    print newBody
##    newParams = ''.join(substitute(list(params), nameToNew))
##    print newParams
##
##    paramToArg = dict(zip(newParams, args))
##    newBody = substitute(newBody, paramToArg)
##
##    extraParams = params[len(args):]
##    if extraParams:
##        return makeFunc(extraParams, newBody)
##    else:
##        return newBody
##
##def reduceOnce(parts, args={}, outerArgs={}):
##    """
##    Perform one round of reduction on parts.
##    
##    args is a mapping of parameters to args, outerArgs is a secondary mapping
##    for arguments bound outside the immediate function.
##    """
##    i = 0
##    newParts = []
##    while i < len(parts):
##        part = parts[i]
##        if isFunc(part):
##            # perform argument substitution into the function
##            params, body = splitFunc(part)
##
##            # get the new args
##            newArgs = parts[i + 1:i + 1 + len(params)]
##            # reduce all compound parts
##            for i, newArg in enumerate(newArgs):
##                if isCompound(newArg):
##                    newArgs[i] = reduceOnce(newArg, args, outerArgs)
####                newArgs[i] = rename(newArg, params)
##            newArgs = dict(zip(params, newArgs))
##
##            print 'new args', newArgs
##            
##            # store any extra parameters
##            extraParams = params[len(newArgs):]
##
##            # current args are added to the outer args
##            newOuterArgs = dict(outerArgs)
##            newOuterArgs.update(args)
##
##            # evaluate the body
##            newBody = reduceOnce(body, newArgs, newOuterArgs)
##
##            if extraParams:
##                # extra parameters left, it's still a function
##                newParts.append(makeFunc(extraParams, newBody))
##            else:
##                # completely evaluated, just another expression now
##                newParts += newBody
##            # start evaluating from the end of the consumed arguments
##            i += len(params)
##        elif isCompound(part):
##            newParts.append(reduceOnce(part, args, outerArgs))
##        elif part in args:
##            newParts.append(args[part])
##        elif part in outerArgs:
##            newParts.append(outerArgs[part])
##        else:
##            newParts.append(part)
##        i += 1
##    
##    return newParts
##
##def reduceExpr(parts):
##    """Reduce a parse tree as much as possible."""
##    while True:
##        newParts = reduceOnce(parts)
##        if newParts == parts:
##            return parts
##        parts = newParts

##def getNameToNew(func, names):
##    """
##    Return a mapping of names to new names that don't exist anywhere in body
##    save inner functions.
##    """
##    nameToNew = dict()
##    namesInFunc = getNames(body, False)
##    for name in names:
##        nameToNew[name] = getNewName(
##                name,
##                namesInFunc | set(nameToNew.values())
##                )
##    return nameToNew

def substitute(body, nameToNew):
    """
    Return body with all names converted according to the mapping in nameToNew,
    unless the name is in an inner function's parameters.
    """
    newBody = []
    for node in body:
        if isFunc(node):
            innerParams, innerBody = splitFunc(node)
            innerNameToNew = dict(nameToNew)
            # remove all the names that exist in innerParams
            for name in innerParams:
                try:
                    del innerNameToNew[name]
                except KeyError:
                    pass
            newBody.append(makeFunc(
                    innerParams,
                    substitute(innerBody, innerNameToNew)
                    ))
        elif isCompound(node):
            newBody.append(substitute(node, nameToNew))
        elif node in nameToNew:
            newBody.append(nameToNew[node])
        else:
            newBody.append(node)

    return newBody

##def convertFunc(func, args):
##    """
##    Perform alpha-conversion on func, changing parameter names and body to not
##    contain any names in argument list.
##
##    >>> convertFunc(['/ab', ['a', 'b']], ['a', 'b'])
##    None
##    >>> convertFunc(['/ab', ['a', ['/ab', ['a', 'b']]]], ['a', 'b'])
##    None
##    >>> convertFunc(['/ab', ['a', ['/cb', ['a', 'b', 'c']]]], ['b', 'a'])
##    >>> convertFunc(['/ab', ['a', ['/ab', ['a', 'b']]]], [['/a', ['a', 'b']]])
##    ['/ab', ['a', ['/ab', ['a', 'b']]]]
##    """
##    params, body = splitFunc(func)
##
##    argNames = getNames(args, False)
##
##    nameToNew = getNameToNew(body, argNames)
##
##    # substitute new names into parameters
##    newParams = ''.join(nameToNew[param] if param in nameToNew else param \
##            for param in params )
##
##    return makeFunc(newParams, newBody)

def reduceOnce(node):
    """
    Reduce an expression once; this basically means performing one round of
    beta-reduction.

    >>> reduceOnce([['/x', 'x'], 'x'])
    'x'
    >>> reduceOnce([['/xyz', [['/x', ['x', 'y']], 'y', 'z', 'x']], [['/y', ['y']], 'y', 'x']])
    None
    """
    if isName(node):
        return node

    if isFunc(node):
        params, body = splitFunc(node)
        return makeFunc(params, reduceOnce(body))

    i = 0
    newNode = []
    while i < len(node):
        innerNode = node[i]
        if isFunc(innerNode):
            params, body = splitFunc(innerNode)

            args = node[i + 1: i + 1 + len(params)]
            args = [reduceOnce(arg) for arg in args]

            if not args:
                newNode.append(innerNode)
            else:
                newNode.append(applyFunc(innerNode, args))
            i += len(params)
        else:
            newNode.append(reduceOnce(innerNode))
        i += 1

    return newNode if len(newNode) > 1 else newNode[0]

def applyFunc(func, args):
    """
    Perform beta-reduction with optional alpha-conversion if needed.

    >>> applyFunc(['/xyz', ['x', 'y', 'z']], ['z'])
    None

    >>> applyFunc(['/xyz', ['x', 'y', 'a']], ['a'])
    ['/yz', ['a', 'y', 'a']]

    >>> applyFunc(['/xyz', ['x', 'y', 'z']], ['z', 'z', 'z'])
    ['z', 'z', 'z']

    >>> applyFunc(['/xyz', [['/x', ['x', 'y']], 'y', 'z', 'x']],
    ... [[['/y', ['y']], 'y', 'x']])
    None
    """
    params, body = splitFunc(func)

    argNames = getNames(args)

    paramToArg = dict(zip(params, args))

    extraParams = params[len(args):]
    # replace all the parameters that occur in the arguments and aren't bound to
    # a value
    toReplace = set(extraParams) & argNames

    bodyNames = getNames(body, withFuncParams=True)

    replacedToNew = dict()
    for replaced in toReplace:
        replacedToNew[replaced] = getNewName(
                replaced,
                bodyNames | set(params) | set(replacedToNew.values())
                )
    # treat the replacement parameters as regular arguments
    paramToArg.update(replacedToNew)

    # perform the replacement
    newBody = substitute(body, paramToArg)
    if extraParams:
        newParams = ''.join(substitute(list(extraParams), paramToArg))
        return makeFunc(newParams, newBody)
    else:
        return newBody if len(newBody) > 1 else newBody[0]

def getNames(node, withFuncParams=False, withFuncBodies=True):
    """
    Return a set of names contained in node.
    
    If withFuncParams, include function parameters.

    If withFuncBodies, include names in function bodies that aren't parameters.
    """
    if isName(node):
        return set(node)
    elif isFunc(node):
        params, body = splitFunc(node)

        result = set()
        if withFuncParams:
            result |= set(params)
        if withFuncBodies:
            result |= getNames(body, withFuncParams, withFuncBodies) \
                    - set(params)
        return result

    return reduce(
            set.union,
            (getNames(innerNode, withFuncParams, withFuncBodies) \
                    for innerNode in node),
            set()
            )

def reduceExpr(node):
    """Reduce an expression as much as possible."""
    while True:
        newNode = reduceOnce(node)
        print newNode
        if node == newNode:
            return node
        node = newNode

if __name__ == '__main__':
    import doctest

    import parser

    # doctest is used here, but should return errors.
    
    # Because some outputs are not guaranteed to be a certain expression but
    # instead satisfy certain properties (like convertFunc()), they should be
    # verified by hand.
    
    # These are indicated by None as a "correct" output.
    doctest.testmod()

    while True:
        try:
            print parser.unparse(
                    reduceExpr(parser.parse(raw_input('>>> ')))
                    )
        except Exception as err:
            print 'Error:', err

##    parts = [['/xyz', ['x', 'y', 'z']], [['/y', ['y']], 'y', 'x']]
##    parts = [['/xyz', [['/x', ['x', 'y']], 'y', 'z']], [['/y', ['y']], 'y', 'x']]
##
##    f = ['/xyz', [['/x', ['x', 'y']], 'y', 'z', 'x']]
##    print 'orig', f, ['y', 'x']
##    print reduceFunc(f, ['y', 'x'])
